Close GREEN-3 with target-specific protocol checking - #13

Purpose

Close RED-3 with the minimum state/transition semantics needed to distinguish protocol-valid from protocol-invalid realizations.

RED-3 showed that two executions can carry the same GREEN-2-correct resource and representation while differing only in protocol trace.

GREEN-3 introduces:

• a generic ProtocolModel(State, Step);
• recursive trace execution via runProtocol;
• an executable checkProtocol relation;
• a composed GREEN-3 gate that requires GREEN-2 correctness plus protocol acceptance.

Not a magic list

The PVM32 witness defines transitions:

operational --enter-config--> config
config      --issue-write--> awaiting-ACK
awaiting-ACK --observe-ACK--> config
config      --exit-config--> operational

All other transitions fail closed.

The checker executes traces through that transition system instead of comparing against one hard-coded accepted sequence.

Machine-checked target

GREEN2(reference) = true
GREEN2(mutated)   = true

GREEN3(reference) = true
GREEN3(mutated)   = false

The PR also proves generically:

checkProtocol(model, trace) = true
    <->
protocolAccepts(model, trace)

Claim boundary

GREEN-3 establishes protocol-sequence correctness only relative to the stated protocol model.

It does not yet prove:

• the ACK came from a concrete device;
• the write persisted;
• timing constraints were met;
• the modeled protocol matches firmware or physical hardware;
• the abstract issueWrite event carries the exact checked payload.

Those remain future falsification targets.